es:event_system{i:l}, e,e':es-E(es).
(loc(e) = loc(e')  Id)  (es-le(es; e; e')  (es-locl(es; e'; e))) 

latex

Definitions	P  Q, P  Q, P  Q, False, P  Q, es-le(es; e; e'), A, es-locl(es; e; e'), prop{i:l}, Id, loc(e), es-E(es), x:A. B(x), t  T, event_system{i:l}, P  Q, trans(T; x,y.E(x;y)), guard(T)
Lemmas	es-axioms, es-locl-antireflexive, es-locl-trans, event system wf, es-E wf, es-loc wf, Id wf, es-locl wf, not wf, es-le wf